From the investigation, a user with a non-zero discount on GHO debt could enter into a unique state by performing a full repayment of their debt while leaving a small residual amount of dust, due to a non-deterministic rounding issue. In this state, they were able to withdraw GHO tokens up to the permitted loan-to-value (LTV) limit repeatedly without adversely affecting the user’s position, potentially allowing them to access GHO tokens up to the capacity of the Aave Facilitator.
Given the complexity and non-deterministic nature of achieving this specific state this issue was not detected during the various stages of development and testing for the project. These phases involved comprehensive analysis, rigorous testing, simulations, and security reviews conducted by the Aave Companies, as well as contributions from the broader community, including entities such as BGD Labs, Sigma Prime, Certora, among others.
We are actively collaborating with Certora to enhance the properties and invariants aspect of the Formal Verification for GHO. This effort aims to better identify edge cases where factors from the Aave Pool and GHO interact in unexpected ways. The forthcoming Formal Verification contest for GHO contracts will play a pivotal role in driving these improvements.
Furthermore, it is imperative to extend our appreciation for the collaboration and diligence exhibited by the individual who initially highlighted an issue on the frontend, which ultimately led to the discovery of the underlying problem. Their proactive involvement, although not a direct report, was instrumental in bringing this matter to our attention. Subsequently, with their assistance and the ongoing cooperation of BGD Labs and Certora, we were able to pinpoint and, effectively, resolve the root issue.
In recognition of their valuable contribution to the protocol’s security and stability, we recommend that the DAO consider awarding a bounty of 50,000 USDC to this individual. It is worth noting that while their input may not align precisely with the conventional definition of a vulnerability report, their insights were of paramount importance in instigating an internal investigation.